Inference at * 
Iof proof for Lemma inl-do-apply:


  A, B:Type, f:(A(B + Top)), x:A. (can-apply(f;x))  ((inl do-apply(f;x) ) ~ (f(x))) 

latex

 by (((UnivCD) 
CollapseTHENA (Auto)) 
CollapseTHEN (MoveToConcl (-1))) 
CollapseTHEN ((
CUnfolds ``can-apply do-apply`` ( 0)) 
CollapseTHEN (((GenConclAtAddr [1;1;1]) 
CollapseTHENA (
CAuto)) 
CollapseTHEN ((D (-2)) 
CollapseTHEN ((Reduce 0) 
CollapseTHEN (Auto)))))
C 

latex

C.

Definitions	Type, can-apply(f;x), do-apply(f;x), f(a), Top, s = t, x:A. B(x), x:AB(x), left + right, True, b, P  Q, t  T, False
Lemmas	true wf, false wf